FDL - Step of Proof: simple-primrec-add

Step of Proof: simple-primrec-add

Inference at *
Iof proof for Lemma simple-primrec-add:

b, F:Top, n, m:

. primrec(n+m;b;

i.F) ~ primrec(n;primrec(m;b;

i.F);

i.F)

by (InductionOnNat)

CollapseTHEN ((Reduce 0)

CollapseTHEN (((D (0)

)

CollapseTHENA (Auto

)

)

CollapseTHEN (((Try ((Complete ((ProveSqEq)

CollapseTHEN (Auto

)

))

))

)

CollapseTHEN ((

CRW (SubC (RecUnfoldTopC `primrec`)) 0)

CollapseTHEN (((if (((first_nat 2:n)) = 0) then (Repeat (

C(((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0))

)

CollapseTHENA (Auto

)

)

CoCollapseTHEN ((Try ((Complete (Auto'))

))

)

)) else (RepeatFor (first_nat 2:n) ((((if (0

C) =0 then SplitOnConclITE else SplitOnHypITE (0))

)

CollapseTHENA (Auto

)

)

CollapseTHEN (

C(Try ((Complete (Auto'))

))

)

)))

)

CollapseTHEN ((EqCD)

CollapseTHEN ((Reduce 0)

CoCollapseTHEN (((Try (Trivial))

)

CollapseTHEN ((Subst' ((n+m) - 1) ~ ((n - 1)+m) ( 0)

)

CoCollapseTHEN (((Try ((if ((0) = 0) then BackThruSomeHyp else BHyp (0) )

))

)

CollapseTHEN (Auto

C

)

)

)

)

)

)

)

)

)

)

)

C.

Definitions s ~ t, n+m, n - m, #$n, Void, a < b, i j , if b then t else f fi , left + right, Unit, P Q, P & Q, x:A B(x), x:AB(x), (i = j), , b, b, f(a), primrec(n;b;c), SQType(T), {T}, Top, , , {x:A| B(x)} , A B, A, False, P Q, s = t, , -n, x:A. B(x), t T

Lemmas ge wf, nat properties, top wf, nat wf, bool wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf